int main(int argc) {
  printf("%d\n", argc);
  return 0;
}
